/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;
import expression.interval.Interval;

/**
 *
 * @author ddoose
 */
public class Min extends IntExpr {

    public Min(Node n) {
        super(n);
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }

    public Min(Node n, IntExpr[] p) {
        super(n, p);
        current = Domain.UNIVERSE;
        target = Domain.UNIVERSE;
    }

    public boolean same(IntExpr i) {
        return (i instanceof Min) && sameParameters(i);
    }
    
    public void eval() throws UnsatException {
        boolean lb, rb;
        int l, r;
        Domain newD;
        IntExpr e = node.getIntExpr(getParameters().get(0));
        
        // init left
        if (e.current.isLeftBounded()) {
            lb = true;
            l = e.current.getLeftBound();
        }
        else {
            lb = false;
            l = 0;
        }
        
        // init right
        if (e.current.isRightBounded()) {
            rb = true;
            r = e.current.getRightBound();
        }
        else {
            rb = false;
            r = 0;
        }
        
        for (int i = 1; i < getParameters().size(); i++) {
            e = node.getIntExpr(getParameters().get(i));
            // left
            if (lb) {
                if ((e.current.isLeftBounded()) && (e.current.getLeftBound() < l)) {
                    l = e.current.getLeftBound();
                }
                else {
                    lb = false;
                }
            }
            // right
            if (rb && e.current.isRightBounded() && (e.current.getRightBound() < r)) {
                r = e.current.getRightBound();
            }
            else if (e.current.isRightBounded()) {
                rb = true;
                r = e.current.getRightBound();
            }
        }
        
        if (lb && rb) {
            newD = new Domain(l, r);
        }
        else if (lb) {
            newD = new Domain(Interval.createLeftBounded(l));
        }
        else if (rb) {
            newD = new Domain(Interval.createRightBounded(r));
        }
        else {
            newD = Domain.UNIVERSE;
        }
        
        reduceCurrent(newD);
    }
    
    public void propagate() throws UnsatException {
    }
    
    public boolean reduce() {
        // si un seul parametre on supprime le max
        if (getParameters().size() == 1) {
            node.removeIntExpr(this);
            return true;
        }        
        return false;
    }

    public Min clone(Node node) {
        Min min = new Min(node);
        min.clone(this);
        return min;
    }
    
    public String toString() {
        String s = "(min";
        
        for (int i: getParameters()) {
            IntExpr p = node.getIntExpr(i);
            s += " " + p;
        }
        
        s += ")";
        
        return s;
    }
    
    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
